Nuprl Lemma : R-possible-Rplus 0,22
A, B:Realizer, es:ES. Possible(A  B;es)  {Possible(A;es) & Possible(B;es) & A || B} 
latex

Definitionst  T, P  Q, x:A. B(x), A || B, Void, x:A. B(x), Top, D1  D2, x:AB(x), P & Q, PossibleWorld(D;w), ES, s = t, ES(the_w), Prop, A & B, x:A. B(x), FairFifo, World, Possible(R;es), {T}, Realizer, A || B, left  right, [[R]]
LemmasR-possible wf, es realizer wf, R-Feasible-Rplus, fair-fifo wf, possible-world wf, event system wf, w-es wf, possible-world-monotonic, Rplus wf, R-Dsys-Rplus, dsys-sub-join-left, dsys-sub-join-right, R-Dsys wf, R-compat-implies

origin